
structure Core =
struct
datatype Expr = plus of Expr * Expr | times of Expr * Expr | Var of int | Zero;

datatype Cmd = Skip | Asgn of int * Expr | Choice of Cmd * Cmd |
	       Seq  of Cmd * Cmd  | Loop of int * Cmd;

fun highest_var_inE(Var i) = i
  | highest_var_inE(Zero) = 1
  | highest_var_inE(plus(e1,e2)) = Int.max(highest_var_inE e1, highest_var_inE e2)
  | highest_var_inE(times(e1, e2))= Int.max(highest_var_inE e1, highest_var_inE e2);
  

fun highest_var(Skip) = 1
  | highest_var(Asgn(j,e)) = Int.max(j, highest_var_inE e)
  | highest_var(Seq(C1,C2)) = Int.max(highest_var C1, highest_var C2) 
  | highest_var(Choice(C1,C2)) = Int.max(highest_var C1, highest_var C2)
  | highest_var(Loop(l,C)) = Int.max(l, highest_var C);
  
	
local
 fun prtExpr(e:Expr) : string =
     case e of
	    Zero => "0"
       | Var n => ("X" ^ (Int.toString n))
       | (plus(e1, e2)) => prtExpr(e1) ^ " + " ^ prtExpr(e2) 
       |(times(e1, e2)) => prtInnerExpr(e1) ^ " * " ^ prtInnerExpr(e2)
 and
  prtInnerExpr(e:Expr) : string =
     case e of
	    Zero => "0"  
	  | Var n => ("X" ^ (Int.toString n))
      | (plus(e1, e2)) => "( " ^ prtInnerExpr(e1) ^ " + " ^ prtInnerExpr(e2) ^ " )"
      | (times(e1, e2)) => "( " ^ prtInnerExpr(e1) ^ " * " ^ prtInnerExpr(e2) ^ " )"

(* print a command. In this version,
  some attention to pretty-printing is done, but no line breaking *)
 fun pprt(c:Cmd) : string =
  case c of
    Skip 		=> "Skip"
  | Asgn(id,e) => (prtExpr (Var id)) ^ " := " ^ (prtExpr e)
  | Choice(s1,s2) => "if ? then " ^ (pprt s1) ^ " else " ^ (pprt s2)
  | Seq(s1,s2) => "{ " ^ (pprtNoBrace s1) ^ "; " ^ (pprtNoBrace s2) ^ " }"
  | Loop(id,s) => "loop " ^ (prtExpr (Var id)) ^ " { " ^ (pprtNoBrace s) ^ " }"
 and
  pprtNoBrace(c:Cmd) : string =
  case c of
    Skip 		=> pprt(c)
  | Asgn(id,e) => (prtExpr (Var id)) ^ " := " ^ (prtExpr e)
  | Choice(s1,s2) => "if ? " ^ " then " ^ (pprt s1) ^ " else " ^ (pprt s2)
  | Seq(s1,s2) => (pprtNoBrace s1) ^ "; " ^ (pprtNoBrace s2) 
  | Loop(id,s) => "loop " ^ (prtExpr (Var id)) ^ " { " ^ (pprtNoBrace s) ^ " }" ;

(* the tagged functions do line-breaking. Receive parameters for indentation and
   line-termination *)
 fun pprt' (indent:string) (finish:string) (c:Cmd) =
  case c of
    Skip 	   => indent ^ pprt(c) ^ finish
  | Asgn(id,e) => indent ^ (prtExpr (Var id)) ^ " := " ^ (prtExpr e) ^ finish
  | Choice(s1,s2) => indent ^ "if ? then\n" ^ (pprt' (indent ^ "  ") "\n" s1) ^
     indent ^ "else\n" ^ (pprt' (indent ^ "  ") finish s2)
  | Seq(s1,s2) => indent ^ "{\n" ^ (pprtNoBrace' (indent ^ "  ") ";\n" s1) ^
      (pprtNoBrace' (indent ^ "  ") "\n" s2) ^ indent ^ "}" ^ finish
  | Loop(id,s) => indent ^ "loop " ^ (prtExpr (Var id)) ^ " {\n" ^
     (pprtNoBrace' (indent ^ "  ") "\n" s) ^ indent ^ "}" ^ finish
 and
  pprtNoBrace' (indent:string) (finish:string) (c:Cmd) =
  case c of
    Skip 	   => indent ^ pprt(c) ^ finish
  | Asgn(id,e) => indent ^ (prtExpr (Var id)) ^ " := " ^ (prtExpr e) ^ finish
  | Choice(s1,s2) => indent ^ "if ? then\n" ^ (pprt' (indent ^ "  ") "\n" s1) ^
     indent ^ "else\n" ^ (pprt' (indent ^ "  ") finish s2)
  | Seq(s1,s2) => (pprtNoBrace' indent ";\n" s1) ^ (pprtNoBrace' indent finish s2) 
  | Loop(id,s) => indent ^ "loop " ^ (prtExpr (Var id)) ^ " {\n" ^
     (pprtNoBrace' (indent ^ "  ") "\n" s) ^ indent ^ "}" ^ finish
in
 (* finally, the pretty-printer chooses whether to do line-breaking or not *)
 fun prt(c:Cmd) : string =
  if (String.size (pprt c)) < 60 then
   (pprt c)^ "\n\n"
  else
	(pprt' "" "\n" c)^ "\n";

 end;
 
end; (* Core *)

